<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="tutorial.css">
<TITLE>
Repair Exercise
</TITLE>
</HEAD>
<BODY >
<A HREF="tutorial096.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial091.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc195">13.6</A>&nbsp;&nbsp;Repair Exercise</H2>
Write a predicate 
<CODE>min_conflicts(Vars,Count)</CODE>
that takes two arguments:
<UL CLASS="itemize"><LI CLASS="li-itemize">
Vars - a list of variables, with tentative 0/1 values
<LI CLASS="li-itemize">Count - a variable, with a tentative integer value
</UL>
The specification of <CODE>min_conflicts(Vars,Count)</CODE> is as follows:
<OL CLASS="enumerate" type=1><LI CLASS="li-enumerate">
If conflict set <CODE>cs</CODE> is empty, instantiate <CODE>Vars</CODE> to
their tentative values 
<LI CLASS="li-enumerate">Otherwise find a variable, <CODE>V</CODE>, in a conflict constraint
<LI CLASS="li-enumerate">Instantiate <CODE>V</CODE> to the value (0 or 1) that maximises
the tentative value of <CODE>Count</CODE> 
<LI CLASS="li-enumerate">On backtracking instantiate <CODE>V</CODE> the other way.
</OL>
This can be tested with the following propositional satisfiability
program.<BR>
<BR>

	<TABLE CELLPADDING=10>
<TR><TD BGCOLOR="#CCCCFF">
	<BLOCKQUOTE CLASS="quote"><PRE>
cons_clause(Clause,Bool) :-
    Clause =:= 1 r_conflict cs,
    Bool tent_is Clause.

prop_sat(Vars,List) :-
    ( foreach(N,List),
      foreach(Cl,Clauses),
      param(Vars)
    do
        cl(N,Vars,Cl)
    ),
    init_tent_values(Vars),
    ( foreach(Cl,Clauses), 
      foreach(B,Bools) 
    do 
      cons_clause(Cl,B)
    ),
    Count tent_is sum(Bools),
    min_conflicts(Vars,Count).

init_tent_values(Vars) :- 
    ( foreach(V,Vars) do V tent_set 1).

cl(1,[X,Y,Z], (X or neg Y or Z)).
cl(2,[X,Y,Z], (neg X or neg Y)).
cl(3,[X,Y,Z], (Y or neg Z)).
cl(4,[X,Y,Z], (X or neg Z)).
cl(5,[X,Y,Z], (Y or Z)).
</PRE></BLOCKQUOTE></TD>
</TR></TABLE><BR>
To test your program try the following queries:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- prop_sat([X,Y,Z],[1,2,3]).
?- prop_sat([X,Y,Z],[1,2,3,4]).
?- prop_sat([X,Y,Z],[1,2,3,4,5]).

</PRE></BLOCKQUOTE>
<HR>
<A HREF="tutorial096.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial091.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
</BODY>
</HTML>
